Groth16 Soundness Proof

7 March 2024 (updated 7 March 2024)

$$ \gdef\delim#1#2#3{\mathopen{}\mathclose{\left#1 #2 \right#3}} \gdef\p#1{\delim({#1})} \gdef\set#1{\delim\{{#1}\}} \gdef\e{\operatorname{e}} \gdef\g{\mathrm{g}} \gdef\Z{\mathrm{Z}} \gdef\U{\mathrm{U}} \gdef\V{\mathrm{V}} \gdef\W{\mathrm{W}} \gdef\k#1{\mathbf{#1}} \gdef\F{\mathbb{F}} \gdef\G{\mathbb{G}} $$

Introduction

Constraints

Recall Groth16. For a given circuit with $n$ variables, $m$ constraints and $p$ public inputs we encode the circuit as $3⋅n+1$ polynomials $\U_i, \V_i, \W_i, \Z ∈ \F[X]$ each with $m$ terms (i.e. degree $m-1$). A witness $x ∈\F^n$ is correct if for some $H(X) ∈ \F[X]$ it satisfies

$$ \p{\sum_{i∈[0,n)} x_i ⋅ \U_i(X)} ⋅ \p{\sum_{i∈[0,n)} x_i ⋅ \V_i(X)} = \p{\sum_{i∈[0,n)} x_i ⋅ \W_i(X)} + H(X) ⋅\Z(X) $$

Setup

During the setup we generate random scalars $τ,α,β,γ,δ$ from $\F$ and compute a set of $\G_1$ and $\G_2$ group elements and promptly forget the original scalars. This leaves us with the following group elements, known to prover and verifier:

$$ \begin{aligned} δ ⋅ \g_1 \\ \set{τ^0, τ^1, τ^2, …, τ^{2 ⋅ m - 2}} ⋅ \g_1 \\ α ⋅ \set{ τ^0, τ^1, τ^2, …, τ^{m - 1} } ⋅ \g_1 \\ β ⋅ \set{τ^0, τ^1, τ^2, …, τ^{m - 1}} ⋅ \g_1 \\ δ^{-1} ⋅ \Z(τ) ⋅ \set{τ^0, τ^1, τ^2, …, τ^{m - 2}} ⋅ \g_1 \\ γ^{-1} ⋅ \set{β ⋅ \U_i(τ) + α ⋅ \V_i(τ) + \W_i(τ)}_{i∈[0,p)} ⋅ \g_1 \\ δ^{-1} ⋅ \set{β ⋅ \U_i(τ) + α ⋅ \V_i(τ) + \W_i(τ)}_{i∈[p,n)} ⋅ \g_1 \\ \end{aligned} $$

$$ \begin{aligned} \set{β, γ, δ} ⋅ \g_2 \\ \set{τ^0, τ^1, τ^2, …, τ^{m - 1} } ⋅ \g_2 \\ \end{aligned} $$

Soundness

To proof soundness we need to show that a verifying proof implies the existence of a witness $x_i$. To do this, we start with what we know. We know the (alleged) prover only knows $\G_1$ values from the setup and can only compute linear combinations of them. So any $\G_1$ value it creates like $A$ has the form (ignoring the $\g_1$ factors)

$$ \begin{aligned} A &= A_τ(τ) + A_α(τ)⋅α + A_β(τ)⋅β + A_δ ⋅ δ + A_γ ⋅ γ + A_Z(τ)⋅{\footnotesize \frac{\Z(τ)}{δ}} \\[0.5em] &\phantom{=}+ \sum_{i∈[0,p)} A_i⋅{\footnotesize \frac{β ⋅ \U_i(τ) + α ⋅ \V_i(τ) + \W_i(τ)}{γ}} + \sum_{i∈[p,m)} A_i⋅ {\footnotesize \frac{β ⋅ \U_i(τ) + α ⋅ \V_i(τ) + \W_i(τ)}{δ} } \\[2em] B &= B_τ(τ) + B_β⋅β + B_δ ⋅ δ + B_γ ⋅ γ \\[0.2em] C &= C_τ(τ) + C_α(τ)⋅α + C_β(τ)⋅β + C_δ ⋅ δ + C_γ ⋅ γ + C_Z(τ)⋅{\footnotesize \frac{\Z(τ)}{δ}} \\[0.5em] &\phantom{=}+ \sum_{i∈[0,p)} C_i⋅{\footnotesize \frac{β ⋅ \U_i(τ) + α ⋅ \V_i(τ) + \W_i(τ)}{γ}} + \sum_{i∈[p,m)} C_i⋅ {\footnotesize \frac{β ⋅ \U_i(τ) + α ⋅ \V_i(τ) + \W_i(τ)}{δ} } \end{aligned} $$

where $A_τ(X)$ has degree at most $2⋅m-2$, $A_α, A_β$ degree at most $m-1$ and $A_Z$ degree at most $m-2$, similarly for $C$. $B(X)$ is of degree at most $m-1$.

Note. In the Groth16 paper no distinction is made between $\G_1$ and $\G_2$ elements and all values are modeled as linear combinations over the (distrete logarithm) of all of them. This hedges against potential easy-to-compute isomorphisms between $\G_1$ and $\G_2$. I'm not doing this to simplify the soundness proof.

We also know that $(w_i, A,B,C)$ pass the verification check, so

$$ A⋅B = α⋅β + \sum_{i∈[0,p)} x_i ⋅ \p{β ⋅ \U_i(τ) + α ⋅ \V_i(τ) + \W_i(τ)} + C⋅δ $$

Since $\F$ is large we can invoke the Schwartz–Zippel lemma and consider both sides as multivariate rational functions in formal parameters $τ,α,β,γ,δ$. We can then group by monomials. Consider equating the following monomials:

$$ \begin{aligned} A_α(τ) ⋅ B_β &= 1 &\hspace{2em}&\p{α⋅β⋅τ^i} \\ A_β(τ) ⋅ B_β &= 0 &\hspace{2em}&\p{β^2⋅τ^i} \\ A_α(τ) ⋅ B_γ &= 0 &\hspace{2em}&\p{α⋅γ⋅τ^i} \\ A_β(τ) ⋅ B_γ + A_γ ⋅ B_β &= 0 &\hspace{2em}&\p{β⋅γ⋅τ^i} \\ \end{aligned} $$

From the first line it follows that $A_α(τ)$ is a non-zero constant and $B_β = A_α^{-1}$. Then by the second and third line $A_β(τ)=0$ and $B_γ = 0$. By the fourth $A_γ = 0$. Then looking at the following monomials

$$ \begin{aligned} \p{\sum_{i∈[0,p)} A_i⋅\p{β ⋅ \U_i(τ) + α ⋅ \V_i(τ) + \W_i(τ)}} ⋅ B_β &= 0 &\hspace{2em}&\p{β⋅γ^{-1}⋅τ^i} \\[2em] \p{A_Z(τ)⋅ \Z(τ) + \sum_{i∈[p,m)} A_i⋅\p{β ⋅ \U_i(τ) + α ⋅ \V_i(τ) + \W_i(τ)}} ⋅ B_β &= 0 &\hspace{2em}&\p{β⋅δ^{-1}⋅τ^i} \\[2em] \end{aligned} $$

We see that these sub-expression from $A$ sum to zero. Substituting all this into $A, B$ gives

$$ \begin{aligned} A &= A_τ(τ) + A_α⋅α + A_δ ⋅ δ \\ B &= B_τ(τ) + A_α^{-1} ⋅ β + B_δ ⋅ δ \end{aligned} $$

Looking at monomials

$$ \begin{aligned} A_α ⋅ B_τ(τ) &= \sum_{i∈[0,p)} x_i ⋅ \V_i(τ) + \sum_{i∈[p,m)} C_i ⋅ \V_i(τ) &\hspace{2em}&\p{α⋅τ^i} \\ A_α^{-1} ⋅ A_τ(τ) &= \sum_{i∈[0,p)} x_i ⋅ \U_i(τ) + \sum_{i∈[p,m)} C_i ⋅ \U_i(τ) &\hspace{2em}&\p{β⋅τ^i} \end{aligned} $$

Defining

$$ \hat x_i=\begin{cases} x_i & i∈[0,p) \\ C_i & i∈[p,m) \end{cases} $$

we can write

$$ \begin{aligned} A_τ(τ) &= A_α ⋅ \sum_{i∈[0,m)} \hat x_i⋅\U_i(τ) \\ B_τ(τ) &= A_α^{-1} ⋅ \sum_{i∈[0,m)} \hat x_i⋅\V_i(τ) \\ \end{aligned} $$

Looking at the monomials $τ^i$:

$$ \p{\sum_{i∈[0,m)} \hat x_i⋅\U_i(τ)} ⋅ \p{\sum_{i∈[0,m)} \hat x_i⋅\V_i(τ)} = \sum_{i∈[0,p)} \hat x_i ⋅ \W_i(τ) + C_Z(τ)⋅\Z(τ) $$

which shows that $\hat x$ is a satisfying witness.

Attempts to get rid of the constant

I'd like to get rid of the constant pairing $\e\p{α⋅\g_1, β⋅\g_2}$. In EVM this requires and additional pairing instead of a target group addition.

Attempt I

Give the verifier $\frac{α⋅β}{γ}⋅\g_1$ to add to the public input point. Since $x_0 = 1$ by convention, this can be done with no extra computation. It also doesn't change the verification equation or the prover algorithm so completeness and zero-knowledge are preserved. However, it does change an attackers abilities as it can now also construct $\G_1$ elements containing an additional term.

$$ \begin{aligned} A' &= A + A_{αβγ} ⋅ \frac{α⋅β}{γ}\\ C' &= C + C_{αβγ} ⋅ \frac{α⋅β}{γ}\\ \end{aligned} $$

We need to check if soundness still holds.

$$ \begin{aligned} A_{αβγ}⋅B_β &= 0 &\hspace{2em}&\p{α⋅β^2⋅γ^{-1}} \\ \end{aligned} $$

From this either $A_{αβγ} = 0$ or $B_β = 0$. Since $A_{αβγ} = 0$ mimics the previous soundness proof, let's proceed with $B_β = 0$ instead and see if it results in contradiction.

$$ \begin{aligned} A_{αβγ}⋅B_γ &= 1 &\hspace{2em}&\p{α⋅β} \\ \end{aligned} $$

From this follows $A_{αβγ} = B_γ^{-1}$ and specifically both are non-zero.

$$ \begin{aligned} A_γ⋅B_γ &= 0 &\hspace{2em}&\p{γ^2} \\ A_α(τ)⋅B_γ &= 0 &\hspace{2em}&\p{α⋅γ} \\ A_β(τ)⋅B_γ &= 0 &\hspace{2em}&\p{β⋅γ} \\ B_τ(τ)⋅B_γ^{-1} &= 0 &\hspace{2em}&\p{α.β⋅γ^{-1}} \\ \end{aligned} $$

From this follows that $A_γ, A_α,A_β,B_τ$ are all $0$.

$$ \begin{aligned} A_τ(τ)⋅B_γ &= 0 &\hspace{2em}&\p{γ} \\ \end{aligned} $$

From this follows that $A_τ = 0$. Finally we have

$$ \begin{aligned} \p{\sum_{i∈[p,m)} A_i ⋅ \V_i(τ)}⋅B_γ &= 0 &\hspace{2em}&\p{α⋅δ^{-1}⋅γ} \\ \p{\sum_{i∈[p,m)} A_i ⋅ \U_i(τ)}⋅B_γ &= 0 &\hspace{2em}&\p{β⋅δ^{-1}⋅γ} \\ \p{\sum_{i∈[p,m)} A_i ⋅ \W_i(τ)}⋅B_γ &= 0 &\hspace{2em}&\p{δ^{-1}⋅γ} \\ \end{aligned} $$

So all these sum to zero, we then get

$$ \begin{aligned} A_Z(τ) ⋅ \Z(τ)⋅B_γ &= 0 &\hspace{2em}&\p{β⋅δ^{-1}⋅γ} \\ \end{aligned} $$

So $A_Z(τ) ⋅ \Z(τ) = 0$.

We're now left with

$$ \begin{aligned} A &= A_δ ⋅δ + B_γ^{-1}⋅\frac{α⋅β}{γ} + \sum_{i∈[0,p)} A_i⋅ \frac{β ⋅ \U_i(τ) + α ⋅ \V_i(τ) + \W_i(τ)}{γ} \\ B &= B_δ ⋅ δ + B_γ ⋅ γ \end{aligned} $$

Let's look at $C$ a bit

$$ \begin{aligned} 0 &= C_τ(τ) &\hspace{2em}&\p{δ} \\ 0 &= C_α(τ) &\hspace{2em}&\p{α⋅δ} \\ 0 &= C_β(τ) &\hspace{2em}&\p{β⋅δ} \\ A_δ ⋅ B_δ &= C_δ &\hspace{2em}&\p{δ^2} \\ A_δ ⋅ B_γ &= C_γ &\hspace{2em}&\p{δ⋅γ} \\ B_γ^{-1} ⋅ B_δ &= C_{αβγ} &\hspace{2em}&\p{α⋅β⋅δ⋅γ^{-1}} \\ \p{\sum_{i∈[0,p)} A_i ⋅ \V_i(τ)}⋅B_δ &= \sum_{i∈[0,p)} C_i ⋅ \V_i(τ) &\hspace{2em}&\p{α⋅δ⋅γ^{-1}} \\ \p{\sum_{i∈[0,p)} A_i ⋅ \U_i(τ)}⋅B_δ &= \sum_{i∈[0,p)} C_i ⋅ \U_i(τ) &\hspace{2em}&\p{β⋅δ⋅γ^{-1}} \\ \p{\sum_{i∈[0,p)} A_i ⋅ \W_i(τ)}⋅B_δ &= \sum_{i∈[0,p)} C_i ⋅ \W_i(τ) &\hspace{2em}&\p{δ⋅γ^{-1}} \\ \end{aligned} $$

This gives us

$$ \begin{aligned} C &= A_δ ⋅ B_δ ⋅ δ + A_δ ⋅ B_γ ⋅ γ + B_γ^{-1} ⋅ B_δ ⋅ \frac{α⋅β}{γ}+ C_Z(τ)⋅{\footnotesize \frac{\Z(τ)}{δ}} \\[0.5em] &\phantom{=}+ B_δ ⋅\sum_{i∈[0,p)} A_i⋅{\footnotesize \frac{β ⋅ \U_i(τ) + α ⋅ \V_i(τ) + \W_i(τ)}{γ}} + \sum_{i∈[p,m)} C_i⋅ {\footnotesize \frac{β ⋅ \U_i(τ) + α ⋅ \V_i(τ) + \W_i(τ)}{δ} } \end{aligned} $$

$$ \begin{aligned} B_δ⋅B_γ^{-1} &= B_β⋅B_γ^{-1} &\hspace{2em}&\p{α⋅β⋅δ⋅γ^{-1}} \\ \end{aligned} $$

So $B_β = B_δ$.

$$ \begin{aligned} B_γ ⋅ \sum_{i∈[0,p)} A_i ⋅ \V_i(τ) &= \sum_{i∈[0,p)} x_i ⋅ \V_i(τ) + \sum_{i∈[p,m)} C_i ⋅ \V_i(τ) &\hspace{2em}&\p{α} \\ B_γ ⋅ \sum_{i∈[0,p)} A_i ⋅ \U_i(τ) &= \sum_{i∈[0,p)} x_i ⋅ \U_i(τ) + \sum_{i∈[p,m)} C_i ⋅ \U_i(τ) &\hspace{2em}&\p{β} \\ \end{aligned} $$

The obvious solution to this is $A_i = B_γ^{-1} ⋅ x_i$ and $C_i = 0$.

To do. Are there non-obvious solutions?

$$ \begin{aligned} B_γ ⋅ \sum_{i∈[0,p)} A_i ⋅ \W_i(τ) &= C_Z(τ) ⋅ \Z(τ) + \sum_{i∈[0,p)} x_i ⋅ \W_i(τ) + \sum_{i∈[p,m)} C_i ⋅ \W_i(τ) &\hspace{2em}&\p{τ} \\ \end{aligned} $$

from this it follows $C_Z = 0$. This dismisses the last term without creating a witness. Instead we found a way to generate 'proofs' for any public input $x_i$

$$ \begin{aligned} A &= A_δ ⋅δ + B_γ^{-1}⋅\p{\frac{α⋅β}{γ} + \sum_{i∈[0,p)} x_i⋅ \frac{β ⋅ \U_i(τ) + α ⋅ \V_i(τ) + \W_i(τ)}{γ}} \\ B &= B_δ ⋅ δ + B_γ ⋅ γ \\ C &= A_δ ⋅ B_δ ⋅ δ + A_δ ⋅ B_γ ⋅ γ + B_γ^{-1} ⋅ B_δ \p{\frac{α⋅β}{γ} + \sum_{i∈[0,p)} x_i⋅{\footnotesize \frac{β ⋅ \U_i(τ) + α ⋅ \V_i(τ) + \W_i(τ)}{γ}} } \end{aligned} $$

The simplest instance of this is

$$ \begin{aligned} A &= \frac{α⋅β}{γ} + \sum_{i∈[0,p)} x_i⋅ \frac{β ⋅ \U_i(τ) + α ⋅ \V_i(τ) + \W_i(τ)}{γ} \\ B &= γ \\ C &= 0 \end{aligned} $$

Attempt II

What if we gave $\frac{α⋅β}{δ}⋅\g_1$ instead? This can be added by the prover or verifier to $C$. It is not possible to construct

$$ \sum_{i∈[0,p)} x_i⋅ \frac{β ⋅ \U_i(τ) + α ⋅ \V_i(τ) + \W_i(τ)}{δ} \\ $$

using the provided setup variables, so the previous break will not work.

Attempt III

Since adding to $L$ or $C$ is not an option, so if it is at all possible the constant will need to be folded into $A⋅B$ somehow. The challenge here is that adding any term to either produces many cross-terms.

Since there is no $α⋅\g_2$ we can try $\frac{α⋅β}{α}⋅\g_1$. But this is just $β⋅\g_1$ which we already had. This suggests simply removing $α⋅β$ from the verification equation:

$$ A ⋅ B = \sum_{i∈[0,p)} x_i ⋅ \p{β ⋅ \U_i(τ) + α ⋅ \V_i(τ) + \W_i(τ)} + C⋅δ $$